{-# LANGUAGE TypeFamilies, GADTs, QuasiQuotes, TypeOperators, ScopedTypeVariables, MultiParamTypeClasses, FlexibleContexts, TemplateHaskell, UndecidableInstances, FlexibleInstances #-}

module Data.Yoko.ZipperHelp (module Data.Yoko.ZipperHelp, module Data.Yoko, module Data.Yoko.Core) where

import Type.Spine
import qualified Type.Ord as Ord

import Data.Yoko hiding (RM(..), (:*), Rep, V, U, D, R, F, FF, M, AF, N, Gst, Gist(..))
import Data.Yoko.Core hiding (Generic(..))

type family Fst a; type instance Fst (a, b) = a
type family Snd a; type instance Snd (a, b) = b

type FieldRep fd = Index (Snd fd) (Rep (Fst fd))

data S n; data Z

type family Take n c
type instance Take Z c = U
type instance Take (S n) (c :* d) = c :* Take n d

type family Drop n c
type instance Drop Z c = c
type instance Drop (S n) (c :* d) = Drop n d

type family Index n c
type instance Index Z (c :* d) = c
type instance Index (S n) (c :* d) = Index n d

type family Append a b
type instance Append U b = b
type instance Append (c :* d) b = c :* Append d b

type family Len c
type instance Len U = Z
type instance Len (c :* d) = S (Len d)

data LT n c where LT_Z :: LT Z (c :* d); LT_S :: LT n d -> LT (S n) (c :* d)

class LessThan n c where lessThan :: LT n c
instance LessThan Z (c :* d) where lessThan = LT_Z
instance LessThan n d => LessThan (S n) (c :* d) where lessThan = LT_S lessThan                            

lessThan_ :: LessThan n c => [qP|n|] -> LT n c; lessThan_ _ = lessThan

appendAFs :: LT n c -> Take n c -> Index n c -> Drop (S n) c -> c
appendAFs LT_Z U x post = x :* post
appendAFs (LT_S lt) (a :* b) x post = a :* appendAFs lt b x post

data Fds c where FdsZ :: Fds U; FdsS :: Gist c => Fds d -> Fds (c :* d)
instance U ::: Fds where inhabits = FdsZ
instance (Gist c, d ::: Fds) => (c :* d) ::: Fds where inhabits = FdsS inhabits



type family Gsts c
type instance Gsts U = U
type instance Gsts (c :* d) = Gst c :* Gsts d

gsts :: (c ::: Fds) => c -> Gsts c
gsts = w inhabits where
  w :: Fds c -> c -> Gsts c
  w FdsZ _ = U
  w (FdsS x) (c :* d) = gist c :* w x d

frips :: (c ::: Fds) => Gsts c -> c
frips = w inhabits where
  w :: Fds c -> Gsts c -> c
  w FdsZ _ = U
  w (FdsS x) (c :* d) = frip c :* w x d

type TakeGsts n dc = Gsts (Take n (Rep dc))
type DropGsts n dc = Gsts (Drop n (Rep dc))





type SameTyConP t s = SameTyConP_ (Spine ([qK|*|] t)) (Spine ([qK|*|] s))
type family SameTyConP_ st ss
type instance SameTyConP_ (a :@ b) ss = SameTyConP_ (Spine a) ss
type instance SameTyConP_ (TypeName n) (a :@ b) = SameTyConP_ (TypeName n) (Spine a)
type instance SameTyConP_ (TypeName n) (TypeName m) =
  IsEQ (Ord.Compare (TypeName n) (TypeName m))

data NotSameTyConU t s where
  NotSameTyConU :: (False ~ SameTyConP t s) => NotSameTyConU t s
obvious_inhabitation ''NotSameTyConU
